let S, T be non empty RelStr ; :: thesis: for f being set holds

( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) )

hence for f being set holds

( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) ) by A1; :: thesis: verum

( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) )

A1: now :: thesis: for S, S1, T, T1 being RelStr st the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 holds

for a being Connection of S,T holds a is Connection of S1,T1

( S ~ = RelStr(# the carrier of S,( the InternalRel of S ~) #) & T ~ = RelStr(# the carrier of T,( the InternalRel of T ~) #) )
;for a being Connection of S,T holds a is Connection of S1,T1

let S, S1, T, T1 be RelStr ; :: thesis: ( the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 implies for a being Connection of S,T holds a is Connection of S1,T1 )

assume A2: ( the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 ) ; :: thesis: for a being Connection of S,T holds a is Connection of S1,T1

let a be Connection of S,T; :: thesis: a is Connection of S1,T1

consider f being Function of S,T, g being Function of T,S such that

A3: a = [f,g] by WAYBEL_1:def 9;

reconsider g = g as Function of T1,S1 by A2;

reconsider f = f as Function of S1,T1 by A2;

a = [f,g] by A3;

hence a is Connection of S1,T1 ; :: thesis: verum

end;assume A2: ( the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 ) ; :: thesis: for a being Connection of S,T holds a is Connection of S1,T1

let a be Connection of S,T; :: thesis: a is Connection of S1,T1

consider f being Function of S,T, g being Function of T,S such that

A3: a = [f,g] by WAYBEL_1:def 9;

reconsider g = g as Function of T1,S1 by A2;

reconsider f = f as Function of S1,T1 by A2;

a = [f,g] by A3;

hence a is Connection of S1,T1 ; :: thesis: verum

hence for f being set holds

( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) ) by A1; :: thesis: verum