let x be set ; for f, g being Function st x in [:f,g:] holds
x = [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]]
let f, g be Function; ( x in [:f,g:] implies x = [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] )
set F = [:f,g:];
set y = x `1 ;
set z = x `2 ;
set x1 = (x `1) `1 ;
set x2 = (x `1) `2 ;
set x3 = (x `2) `1 ;
set x4 = (x `2) `2 ;
assume A1:
x in [:f,g:]
; x = [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]]
then reconsider F = [:f,g:] as non empty Function ;
F <> {}
;
then reconsider ff = f as non empty Function ;
F <> {}
;
then reconsider gg = g as non empty Function ;
reconsider F = [:ff,gg:] as non empty Function by A1;
reconsider xx = x as Element of F by A1;
reconsider y = xx `1 , z = xx `2 as pair object ;
( y = [(y `1),(y `2)] & z = [(z `1),(z `2)] & xx = [(xx `1),(xx `2)] )
;
hence
x = [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]]
; verum